package preprocessor.absorption;

import java.util.HashSet;
import java.util.Set;
import java.util.Stack;

import option.KBVocabulary;

import preprocessor.Simplification;
import utils.exception.ConceptException;

import kb.TBox;

import entities.concept.AndConcept;
//import entities.concept.AtomicConcept;
import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
import entities.concept.PConcept;
import entities.concept.UniversalConcept;
import entities.role.Role;

public class InverseRoleAbsorption implements Absorption {
	private TBox tbox;

	public InverseRoleAbsorption(TBox tb) {
		this.tbox = tb;
	}

	public boolean absorb() {
		boolean suc = true;
		Set<Concept> cs = new HashSet<Concept>();
		Set<Concept> topadded = new HashSet<Concept>();
		boolean topChanged = false;
		for (Concept c : this.tbox.getTg().keySet()) {
			Concept rhs = this.tbox.getTg().get(c);
			if (c.isTop()) {
				// top -> C1 and C2 and ... and Cn, absorb Ci separately.
				for (Concept each : Concept.reduceToConjuncts(rhs)) {
					boolean part = this.absorbAxiom(Concept
							.reduceToDisjuncts(each));
					if (!part) {
						topadded.add(each);
					} else {
						topChanged = true;
						suc = true;
					}
				}
			} else {
				// add ~lhs or rhs
				Set<Concept> args = new HashSet<Concept>();
				args.add(Simplification.NNF(c, true));
				args.add(rhs);
				if (this.absorbAxiom(args)) {
					cs.add(c);
					suc = true;
				}
			}
		}
		for (Concept cc : cs) {
			this.tbox.getTg().remove(cc);
		}
		// modify top GCI
		if (topChanged) {
			if (topadded.size() == 1) {
				this.tbox.getTg().put(KBVocabulary.CONCEPT_TOP,
						topadded.iterator().next());
			} else if (topadded.size() > 1) {
				this.tbox.getTg().put(KBVocabulary.CONCEPT_TOP,
						new AndConcept(topadded));
			} else {
				// remove this top GCI
				this.tbox.getTg().remove(KBVocabulary.CONCEPT_TOP);
			}
		}
		return suc;
	}

	private boolean absorbAxiom(Set<Concept> cs) {
		UniversalConcept uc = null;
		PConcept ucf = null;
		for (Concept c : cs) {
			if (c instanceof UniversalConcept) {
				ucf = this.extracUC((UniversalConcept) c);
				if (ucf != null) {
					uc = (UniversalConcept) c;
					break;
				} else {
					continue;
				}
			}
		}
		if (uc != null) {
			// start to absorb
			cs.remove(uc);
			Concept rhs = null;
			if (cs.size() == 1) {
				rhs = cs.iterator().next();
			} else if (cs.size() > 1) {
				rhs = new OrConcept(cs);
			} else {
				// don't absorb top-> all R.S
				return false;
			}
			PConcept annoc = PConcept.newInternalPConcept();
			Stack<Role> rs = this.formInverse(uc);
			Concept abs = annoc;
			while (!rs.isEmpty()) {
				Role ir = this.tbox.getRoleBox().getInverseRole(rs.pop());
				abs = new UniversalConcept(ir, abs);
			}
			// add axiom 1: A' -> disjunctions
			try {
				this.tbox.insertTu(annoc, rhs);
			} catch (ConceptException e) {
				e.printStackTrace();
			}
			// add axiom 2: filler -> all T-.....all S-.all R-.A'
			try {
				this.tbox.insertTu(ucf, rhs);
			} catch (ConceptException e) {
				e.printStackTrace();
			}
			return true;
		}
		return false;
	}

	// modified algorithm: see KR12, accept only:
	// all R. all S. ... all T. (not A)
	private PConcept extracUC(UniversalConcept uc) {
		Concept fc = uc.getFiller();
		if (fc instanceof UniversalConcept) {
			return this.extracUC((UniversalConcept) fc);
		} else if (fc instanceof NotConcept) {
			NotConcept nc = (NotConcept) fc;
			if (nc.getConcept() instanceof PConcept) {
				if (Absorption.NCA && this.tbox.getTnu().containsKey(nc)) {
					return null;
				} else {
					return (PConcept) nc.getConcept();
				}
			}
		}
		return null;
	}

	private Stack<Role> formInverse(UniversalConcept uc) {
		Stack<Role> rs = new Stack<Role>();
		Concept c = uc;
		while (c instanceof UniversalConcept) {
			rs.push(uc.getRole());
			c = uc.getFiller();
		}
		return rs;
	}

}
